w:World. FairFifo  (e:E. state_after(e)  x:Idvartype(loc(e);x)) 

latex

Definitions	x:A. B(x), P  Q, t  T, vartype(i;x), state_after(e), EState(T), A, , A  B, False, t.1, t.2, S  T, suptype(S; T), x. t(x), x,y. t(x;y), loc(e), V(i;k), kind(e), act(e), time(e), SWellFounded(R(x;y)), x:A. B(x), , w-automaton(T;TA;M), x(s), x(s1,s2), E, w.TA, w.M
Lemmas	state after wf, w-T wf, w-TA wf, w-M wf, w-pred wf, w-info wf, w-s wf, le wf, Id wf, w-loc-lemma, pred wf, w-loc-pred, not wf, assert wf, first wf, w-E wf, fair-fifo wf, world wf, w-machine wf, w-automaton wf, Knd wf, kindcase wf, IdLnk wf, rationals wf, w-vartype wf, w-eval wf, w-kind-lemma, subtype rel self, w-kind wf, w-a wf, int-rational, w-time wf, nat wf, w-pred!-decreases, pred! wf